T:Type, L:(T List). ((null(L)))  (last(L)  T) 

latex

Definitions	last(L), t  T, P  Q, x:A. B(x), False, prop{i:l}, gt(i; j), A  B, A, P  Q, P  Q
Lemmas	null wf, assert wf, not wf, length wf1, select wf, non nil length, assert of null, not functionality wrt iff